package systemfnomabss


/**
  * As per TAPL 
  *
  */
  


trait systemfEvaluator extends Evaluator  { self: systemfEvaluator with TermSubstitutionProvider with AbstractSyntax=>

  def evaluate(t: LTerm) : LTerm = t match {
      case v if isValue(v) => v
      case morework => evaluate(eval1(morework)) 
  } 

  
  
  def eval1(t: LTerm): LTerm = t match {
    //E-IfTrue, E-IfFalse
    case If(c,p,n) if (isValue(c))            
      => if (c equals Tru()) p else n
    //E-If
    case If(c,p,n)
      => If(eval1(c),p,n)
    
    //E-AppAbs
    case App( Lam(ty, x\\t12), v2) if (isValue(v2))
      => substituteterm(v2).as(x).intoterm(t12)    
    //E-App2 
    case App(v1, t2)             if (isValue(v1))  
      => App(v1 ,eval1(t2))
    //E-App1
    case App(t1, t2)                             
      => App(eval1(t1), t2)
    
      
    //E-Let
    case Let(v1,hint\\tbody) if (isValue(v1))  
      => substituteterm (v1) as hint intoterm tbody
    case Let(t1, body)                      
      => Let(eval1(t1), body)
      
      
    //E-TAppAbs
    case TApp( TLam(s\\t12), ty)                    
      => substitutetype (ty) as s  intoterm t12    //or just take body: erasure semantics
    //E-TApp
    case TApp(t1, ty)
      => TApp(eval1(t1), ty)
   
    
      //E-UnpackPack
    case Unpack(Pack(impltype,implvar,pubtype),tyvar_termvar_body) if (isValue(implvar))
       => println("E-UnpackPack on "+t);tyvar_termvar_body match {
        case tyvar  \\termvar_body => termvar_body match {
        case Lam(TyVar(tyvarsynonym), termvar\\body) if tyvar == tyvarsynonym => 
        val substresult =
              substituteterm(implvar)  as termvar intoterm(
              substitutetype(impltype) as tyvar   intoterm(
                                                       body))
        println("subst result = "+substresult);substresult
      //typeintotermSubstTop(impltype, termSubstTop(implvar, body))
      }}
     
    //E-Unpack
    case Unpack(impl,tyvar_termvar_body)
      => Unpack(eval1(impl),tyvar_termvar_body)
      
    //E-Pack
    case Pack(ty11,t12,pubtype)
      => Pack(ty11,eval1(t12),pubtype)
       
    
    //E-RecProj
    case RecProj(r@Record(fields),label) 
      if ( isValue(r))   =>
           fields.filter( { case (n,f) => (n == label)}).map(_ _2).head
    case RecProj(Record(fields), label) =>
      def eval1first(fs:List[(String,LTerm)]) :List[(String,LTerm)]= {
        val h = fs.head
        if (isValue(h._2)) h::eval1first(fs.tail)
        else (h._1,eval1(h._2))::fs.tail
      }
      RecProj(Record(eval1first(fields)), label)
    case RecProj(t, label)                =>
      RecProj(eval1(t), label)
    
      
    case _                                    =>
         throw NoReductionPossibleExc(t)
  }
  
  
  
  def isValue(t: LTerm) : Boolean= t match {
    case Lam(_,_) => true
    case TLam(_)  => true
    case Pack(ty1,v,pubtype) => isValue(v)
    case Lit(v)     => true
    case Tru()      => true
    case Fls()      => true
    case Unit()     => true
    case Record(fields) => fields.map({case (label,comp)=>comp}) forall(isValue)
    case _        => false
  }
  
  
}




